module ABSTRACT_INTERPRETER_ALGORITHM
open System
open FSEvent
open utils

let (@@) g1 g2 = ContextGraph.compose g1 g2 AbstractDomain.prod
let (@@@) g1 g2 = ContextGraph.compose g1 g2 AbstractDomain.prod_for_increment_loop
let (|||) g1 g2 = ContextGraph.joinAsLeastUpperBound g1 g2

(* type AbstractInterpreter encapsulates the abstract interpreter algorithm, as described in abstractInterpreterAlgorithm.docx *)
type AbstractInterpreter() =
    let Debug = ref false

    (* event to notify that a command's graph was updated *)
    [<CLIEvent>]
    member x.CommandGraphUpdated = commandGraphUpdated.Publish

    [<CLIEvent>]
    member x.DebugInfoAdded = debugInfoAdded.Publish

    (* the entry point for the abstact interpreter execution. Recieves a command of the core language as input (in AST form) and
       returns a context-graph which represents the algorithm analysis results on the input command. *)
    member x.analyse(c : Core.Cmd) : ContextGraph.graph =
            (* a global identifier which is updated (at the beginning of the algorithm execution)
           to hold the number of variables in the analysed program. *)
        let numVars = ref 0
        (* an iterator for debug print-out which is increased on each analysis interation over a loop body. *)
        let itCount = ref 0
        (* debug mode -  when true - each algorithm stage will be printed, along with its output (and sometimes input). *)
        (* Sends s to the any debug info added event listener. *)
        let debugPrint(s) = if (!Debug) then debugInfoAdded.Trigger(DebugInfoAddedEventArgs(s))

        let debugPrintG(g) = if (!Debug) then debugPrint(ContextGraph.prtEdges(g))
        (* returns flow i-(1)->i if i is not in source context and i <> x *)
        let computeFlowFromItoI(c : CoreEx.Cmd, i : int, x : int, srcContext : ContextGraph.Context) =
            if (i = x) then
                []
            elif ContextGraph.inResetContext(i, srcContext) || ContextGraph.inConstantContext(i, srcContext) then
                []
            else
                [(i, i, AbstractDomain.copy, CoreEx.pat(c))]

        (* computes context graph for commands of the form "X := 0" or "X := 1" *)
        let computeAsgnContantGraph(c : CoreEx.Cmd, x : int, preContexts : ContextGraph.Context list, constant : Core.Expr) =
            let computeDataFlows(srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                        computeFlowFromItoI(c, i, x, srcContext) @ computeMultipleFlows(i-1, srcContext)

                computeMultipleFlows((!numVars),srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext)

                (* include x in relevant target context *)
                ContextGraph.setVarInConstantContext x tgtContext (constant = Core.One)
                ContextGraph.setVarInResetContext x tgtContext (constant = Core.Zero)

                let m = sparseMatrix.M(computeDataFlows(srcContext))

                ContextGraph.E ( srcContext, tgtContext, (ref (setOfPairs.Dfr(m, sparseMatrix.r(m)))))

            List.map computeEdge preContexts

        (* computes context graph for commands of the form "X := Y" *)
        let computeAsgnVarGraph(c : CoreEx.Cmd, x : int, y : int, preContexts : ContextGraph.Context list) =
            let computeDataFlows(srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeFlowFromYtoX(i : int, srcContext : ContextGraph.Context)  =
                    if i <> y then
                        [] 
                    elif (not (ContextGraph.inResetContext(y, srcContext))) then
                        [(y,x,AbstractDomain.copy,CoreEx.pat(c))]
                    else []

                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                            let flowYtoX = computeFlowFromYtoX(i,srcContext)
                            let flowItoI = computeFlowFromItoI(c,i,x,srcContext)
                            flowYtoX @ flowItoI @ computeMultipleFlows(i-1, srcContext)

                computeMultipleFlows((!numVars), srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext)
                let yInSrcRContext = ContextGraph.inResetContext(y, srcContext)
                let yInSrcCContext = ContextGraph.inConstantContext(y, srcContext)
                (* add x to target context if y is in source context (equivalent to assignment of X := 0 or X := 1),
                    otherwise exclude x from target context (equivalent to assignment of X := Y, where Y <> 0) *)
                let () = ContextGraph.setVarInResetContext x tgtContext yInSrcRContext
                let () = ContextGraph.setVarInConstantContext x tgtContext yInSrcCContext
                let m = sparseMatrix.M(computeDataFlows(srcContext))

                ContextGraph.E ( srcContext, tgtContext, (ref (setOfPairs.Dfr(m, []))))

            List.map computeEdge preContexts

        (* computes context graph for commands of the form "X := Y * Z" *)
        let computeAsgnTimesGraph(c : CoreEx.Cmd, x, y, z, preContexts) =
            let computeDataFlows(srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeSingleFlow(i : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                    (* add flow y-(2)->x (or z-(2)->x) if y and z are both not in the source context (equivalent to assignment of X := Y*Z where Y>0 and Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : ContextGraph.Context) =
                        let yInRContext = ContextGraph.inResetContext(y, srcContext)
                        let zInRContext = ContextGraph.inResetContext(z, srcContext)

                        let yInSrcCContext = ContextGraph.inConstantContext(y, srcContext)
                        let zInSrcCContext = ContextGraph.inConstantContext(z, srcContext)

                        if (i <> y && i <> z) then 
                            []
                        elif (yInRContext || zInRContext) then
                            []
                        elif (yInSrcCContext || zInSrcCContext) then
                            [(i, x, AbstractDomain.copy, CoreEx.pat(c))]
                        else
                            [(i, x, AbstractDomain.polynomial, CoreEx.pat(c))]

                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)

                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                        computeSingleFlow(i, srcContext) @ computeMultipleFlows(i-1, srcContext)

                computeMultipleFlows((!numVars), srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext)
                let y_or_z_in_srcRContext = (ContextGraph.inResetContext(y, srcContext)) || (ContextGraph.inResetContext(z, srcContext))
                let y_or_z_in_srcCContext = (ContextGraph.inConstantContext(y, srcContext)) && (ContextGraph.inConstantContext(z, srcContext))
                (* add x to target context if  y or z are in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y * Z, where Y>0 and Z > 0) *)
                let _ = ContextGraph.setVarInResetContext x tgtContext y_or_z_in_srcRContext
                let _ = ContextGraph.setVarInConstantContext x tgtContext y_or_z_in_srcCContext
                let mat = sparseMatrix.M(computeDataFlows(srcContext))

                ContextGraph.E ( srcContext, tgtContext, (ref (setOfPairs.Dfr(mat, []))))

            List.map computeEdge preContexts


        (* computes context graph for commands of the form "X := Y + Z" *)
        let computeAsgnPlusGraph(c : CoreEx.Cmd, x, y, z, preContexts) =
            let computeDataFlows(x : int, y : int, z : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeSingleFlow(i : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                    (* add flow y-(1')->x (or z-(1')->x) if y (or z) are not in the source context (equivalent to assignment of X := Y+Z where Y>0 or Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : ContextGraph.Context) =
                        let iInSrcRContext = ContextGraph.inResetContext(i,srcContext)
                        let yInSrcRContext = ContextGraph.inResetContext(y, srcContext)
                        let zInSrcRContext = ContextGraph.inResetContext(z, srcContext)

                        let yInSrcCContext = ContextGraph.inConstantContext(y, srcContext)
                        let zInSrcCContext = ContextGraph.inConstantContext(z, srcContext)

                        if (i <> y && i <> z) then
                            []
                        elif (iInSrcRContext || (yInSrcRContext && zInSrcRContext)) then
                            []
                        elif (yInSrcCContext && zInSrcCContext) then (* here we use the knowledge that var 1 is __const*)
                            [(1, x, AbstractDomain.copy, CoreEx.pat(c))]
                        elif (yInSrcRContext || zInSrcRContext) then
                            [(i, x, AbstractDomain.copy, CoreEx.pat(c))]
                        elif (yInSrcCContext || zInSrcCContext) then
                            [(i, x, AbstractDomain.copy, CoreEx.pat(c))]
                        else
                            if y = z then
                                [(i, x, AbstractDomain.linearPolynomial, CoreEx.pat(c))] (* when the same var is added then we deduce polynomial growth *)
                            else
                                [(i, x, AbstractDomain.additive, CoreEx.pat(c))]

                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)

                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                            computeSingleFlow(i,srcContext) @ computeMultipleFlows(i-1,srcContext)

                computeMultipleFlows((!numVars),srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext)
                let y_xor_z_in_srcCContext = (ContextGraph.inConstantContext(y, srcContext)) <> (ContextGraph.inConstantContext(z, srcContext))
                let y_and_z_in_srcRContext = (ContextGraph.inResetContext(y, srcContext)) && (ContextGraph.inResetContext(z, srcContext))
                (* add x to target context if  y and z are both in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y + Z, where Y>0 or Z > 0) *)
                let _ = ContextGraph.setVarInConstantContext x tgtContext y_xor_z_in_srcCContext
                let _ = ContextGraph.setVarInResetContext x tgtContext y_and_z_in_srcRContext
                let m = sparseMatrix.M(computeDataFlows(x,y,z,srcContext))

                ContextGraph.E ( srcContext, tgtContext, (ref (setOfPairs.Dfr(m, sparseMatrix.r(m)))))

            List.map computeEdge preContexts

        (* computes context graph for commands of the form "X := Y + 1" *)
        let computeAsgnPlusOneGraph(c : CoreEx.Cmd, x, y, preContexts) =
            let computeDataFlows(x : int, y : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeSingleFlow(i : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                    let yInSrcCContext = ContextGraph.inConstantContext(y, srcContext)

                    (* add flow y-(1')->x if y are not in the source context *)
                    let computeFlowFromYtoX(i : int, srcContext : ContextGraph.Context) =
                        if i <> y then
                            []
                        elif yInSrcCContext then
                            [(1, x, AbstractDomain.copy, CoreEx.pat(c))]
                        else
                            [(i, x, AbstractDomain.incrementBy1, CoreEx.pat(c))]
                            
                    computeFlowFromYtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)

                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                            computeSingleFlow(i,srcContext) @ computeMultipleFlows(i-1,srcContext)

                computeMultipleFlows ((!numVars), srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                let tgtContext = ContextGraph.copyContext(srcContext)
                let yInsrcRContext = ContextGraph.inResetContext(y, srcContext)

                let _ = ContextGraph.removeVarFromResetContext x tgtContext
                let _ = ContextGraph.setVarInConstantContext x tgtContext yInsrcRContext
                let m = sparseMatrix.M(computeDataFlows(x, y , srcContext))

                ContextGraph.E ( srcContext, tgtContext, (ref (setOfPairs.Dfr(m, sparseMatrix.r(m)))))

            List.map computeEdge preContexts

        (* updates DFRs on all edges of graph g with all possible data flows of the form (i->j,i'->j'). *)
        let computeDoubleFlows g : ContextGraph.graph =
            let updateDoubleFlowsOnEdge = function
                | ( ContextGraph.E(p, q, refDfr) ) ->
                    (* filter function to determine if a given double data flow should be included in the result *)
                    let includeFlow (p : ContextGraph.Context,q : ContextGraph.Context) ((i,j),(i',j'),pat) =
                                    (not (ContextGraph.inResetContext(i,p))) && (not (ContextGraph.inResetContext(i',p))) &&
                                    (not (ContextGraph.inResetContext(j,q))) && (not (ContextGraph.inResetContext(j',q))) &&
                                    (i <> i' || j <> j')
                    match !refDfr with
                    | (setOfPairs.Dfr(m,_)) as dfr ->
                            (* filter double flows according to source and target contexts *)
                            let r' = List.filter (includeFlow(p,q)) (sparseMatrix.r(m))
                            refDfr := setOfPairs.Dfr(m,r')
                | _ ->  failwith "AbstractInterpreter.updateDoubleFlowsOnEdge: Invalid argument."

            List.iter updateDoubleFlowsOnEdge (ContextGraph.getEdges(g))
            g

        (* computes a graph corresponding to the abstract interpretation of an assignment command, with given pre-contexts *)
        let computeAssignmentGraph (c : CoreEx.Cmd, x : int, e : Core.Expr, preContexts : ContextGraph.Context list) : ContextGraph.graph ref =
            (* computes data flows of the form i-(d)->j *)
            let computeSingleFlows (x : int) (e : Core.Expr) (preContexts : ContextGraph.Context list) =
                match e with
                | Core.Zero ->                          computeAsgnContantGraph(c, x, preContexts, Core.Zero)
                | Core.One ->                          computeAsgnContantGraph(c, x, preContexts, Core.One)
                | Core.Var y ->                         computeAsgnVarGraph(c,x, y, preContexts)
                | Core.Times(Core.Var y, Core.Var z) -> computeAsgnTimesGraph(c, x, y, z, preContexts)
                | Core.Plus(Core.Var y , Core.Var z) -> computeAsgnPlusGraph(c, x, y, z, preContexts)
                | Core.Plus(Core.Var y , Core.One)
                | Core.Plus(Core.One , Core.Var y) -> computeAsgnPlusOneGraph(c, x, y, preContexts)
                | _ -> failwith "AbstractInterpreter.computeAssignmentGraph: Invalid argument."
            
            // partition the precontext to two groups: one where the pre-mode is 'normal' and one that equals some label.
            // if the mode is not 'normal', then computeSingleFlows as if the skip command was performed (equal to x := x), else computeSingleFlows with x := e.
            let partitionedByMode = List.partition (fun (m : ContextGraph.Context) -> m.modeCtx <> ContextGraph.Mode.Normal) preContexts

            let SkipedSingleFlows = if (fst partitionedByMode).Length > 0 then
                                        computeSingleFlows 1 (Core.Var 1) <| fst partitionedByMode
                                    else []

            let normalSingleFlows = if (snd partitionedByMode).Length > 0 then
                                        computeSingleFlows x e <| snd partitionedByMode 
                                    else []

            // the resulting graph is the union of these flows.
            let g' = ref (ContextGraph.newGraph (normalSingleFlows @ SkipedSingleFlows))
            (* computes all data flows of the form (i->j,i'->j') over the flows calculated for all edges of the graph g' *)
            ref (computeDoubleFlows(!g'))

        (* abstractly interpret command c,  creating (or updating) its ContextGraph.graph, return ref to resulting graph *)
        let rec abstractInterpret(c : CoreEx.Cmd, preContexts : ContextGraph.Context list) : ContextGraph.graph ref =
            (* Computes the loop correction on all edges where applicable. This function applies loop rule L2 in the DICE paper. *)

            let doLoopCorrection(loopVar : int, g : ContextGraph.graph ref)  =
                (* overload operator * to represent DFR composition, in thie scope of this function only *)
                let (^*) (d1 : setOfPairs.DFR) (d2 : setOfPairs.DFR) : setOfPairs.DFR = setOfPairs.prod d1 d2 AbstractDomain.prod_for_increment_loop

                (* The loop correction operator on DFRs. *)
                let loopCorrection(loopVarIndex, setOfPairs.Dfr(m, r)) =
                    let m' = sparseMatrix.loopCorrection (loopVarIndex, CoreEx.id(c)) m
                    let m'' = sparseMatrix.loopCorrection (loopVarIndex, CoreEx.id(c)) m'
                    let m''' = sparseMatrix.loopCorrectionIncrements (loopVarIndex, CoreEx.id(c)) m''
                    setOfPairs.Dfr(m''', setOfPairs.filterR(r, m'''))

                for preCtx in (!g).Keys do
                    for edge in (!g).[preCtx] do
                        let postCtx = edge.Key
                        for preCtx' in (!g).Keys do
                            for edge' in (!g).[preCtx'] do
                               let postCtx' = edge'.Key
                               if (ContextGraph.eqContexts(postCtx, preCtx')) then
                                   match ContextGraph.getEdgeTag(!g, ContextGraph.UE (postCtx, postCtx)) with
                                              | Some (dfr) ->
                                                            let dfr = edge.Value
                                                            let dfr' = edge'.Value
                                                            if preCtx'.modeCtx = ContextGraph.Mode.Normal then
                                                                let edgeTag = ref ( !dfr ^* loopCorrection(loopVar, !dfr) ^* !dfr')
                                                                let newEdge = ContextGraph.E(preCtx, postCtx', edgeTag)
                                                                ContextGraph.addEdge(!g, newEdge)
                                                            (*compute the loop correction where applicable *)
                                              | None     -> ()

            (* computes result graph of a single loop iteration, provided that the loop body is c and
               that execution of all loop iterations so far have resulted with the graph g. *)
            let doSingleIteration (g : ContextGraph.graph ref, c : CoreEx.Cmd)  =
                let () = debugPrint("=======doSingleIteration=========\nIteration #"  + (!itCount).ToString() + ":\n")
                (* Compute the graph representing the loop body, with pre-contexts which are the post contexts of the current gaph.
                   This is a graph which represents the next iteration of the loop. *)
                let g' = abstractInterpret(c, ContextGraph.postContexts(!g))
                let () = debugPrint("current graph(g):\n")
                let () = debugPrintG(!g)
                let () = debugPrint("graph to compose(g'):\n")
                let () = debugPrintG(!g')
                (* now, compute the composition of current iteration and the next iteration graphs *)
                let g'' = !g @@@ !g'
                let () = debugPrint("composed graph(g''):\n")
                let () = debugPrintG(g'')
                (* now - join the results of last iteration with results of current iteration,
                   and the composition of last result with current iteration *)
                let g''' = !g ||| !g' ||| g''
                let () = debugPrint("join result graph(g'''):\n")
                let () = debugPrintG(g''')
                let () = debugPrint("================================\n")
                let () = itCount := !itCount + 1
                (* return the result graph representing the next loop iteration *)
                g'''

            (* Compute the result graph of any m >0 iterations of the loop whose body is c and the iterator variable is x.
               Update the result graph to g. This function applies loop rule L1 in the DICE paper. *)
            let doLoopClosure(x : int, c : CoreEx.Cmd, g : ContextGraph.graph ref) : ContextGraph.graph ref =
                (* least fixed point function *)
                let rec lfp f (g : ContextGraph.graph ref, c : CoreEx.Cmd) : ContextGraph.graph ref =
                    let () = debugPrint("lfp: g before:\n")
                    let () = debugPrintG(!g)
                    let fg = f(g, c)
                    let isEq = ContextGraph.equal(fg,!g)
                    let () = debugPrint(if (isEq) then "lfp reached!\n" else "lfp not reached!\ng:\n")
                    let () = debugPrintG(!g)
                    let () = debugPrint("fg:\n")
                    let () = debugPrintG(fg)

                    if (isEq) then g else (g := fg
                                           debugPrint("lfp: g after:\n")
                                           debugPrintG(!g)
                                           lfp f (g,c))

                let () = itCount := 0
                lfp doSingleIteration (g,c)

            (* apply the loop rules. The result graph is updated in g *)
            let doLoop(x : int, c : CoreEx.Cmd, preContexts : ContextGraph.Context list, g : ContextGraph.graph ref) : ContextGraph.graph ref =
                (* Partition the precontext list according to: 1. Reset context 2. Constant context *)
                let inclInR, notInclInR = List.partition (fun ctx -> ContextGraph.inResetContext(x ,ctx)) preContexts
                let inclInC, notInclInC = List.partition (fun ctx -> ContextGraph.inConstantContext(x ,ctx)) preContexts

                (* Filter to precontext list to include only precontexts that don't include x (both reset and constant *)
                let notInclInCAndR = List.filter (fun ctx -> not (ContextGraph.inConstantContext(x ,ctx)) && not (ContextGraph.inResetContext(x ,ctx))) preContexts

                (* when there are no pre-contexts, this means that in all
                   possible conditions, the loop bounding variable is zero,
                   hence the loop has no effect. *)
                if List.isEmpty(notInclInR) then
                    let () = g := !computeAssignmentGraph(c, 1,Core.Var 1, inclInR)
                    g
                (* same for constant contexts, but it will be treated as only one iteration *)
                elif List.isEmpty(notInclInC) then
                    abstractInterpret(c, inclInC)
                else
                    (* compute graph representing loop's body, including a possibility of zero iterations (skip).
                        This action also applies loop rule L0 in the DICE paper
                        (since each loop body c was expanded to "if { Skip } else { c }").*)
                    let () = g := !(abstractInterpret(c, notInclInCAndR))
                    (* compute graph representing any m>0 iterations of the loop body *)
                    let _ = doLoopClosure(x, c, g)
                    let () = debugPrint("after loop closure.\n")
                    let () = commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c,!g))
                    let () = doLoopCorrection(x, g)
                    let () = debugPrint("after loop correction.\n")
                    let () = commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c,!g))
                    let () = ContextGraph.filterEdgesByPreContexts(g, notInclInCAndR)
                    let () = debugPrint("after edge filtering.\n")
                    let () = commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c,!g))
                    g

            (* computes the composition result graph of commands c1 and c2 and updates it to g *)
            let doCompose(c1 : CoreEx.Cmd,c2 : CoreEx.Cmd, preContexts : ContextGraph.Context list, g : ContextGraph.graph ref) : ContextGraph.graph ref =
                let g1 =    abstractInterpret(c1, preContexts)
                let g2 = abstractInterpret(c2, (ContextGraph.postContexts(!g1)))
                let () = g := (!g1 @@ !g2)
                g

            (* computes the join(Least Upper Bound) result graph of commands c1 and c2 and updates it to g *)
            let doChoice(c1 : CoreEx.Cmd,c2 : CoreEx.Cmd, preContexts : ContextGraph.Context list, g : ContextGraph.graph ref) : ContextGraph.graph ref =
                let () = g := (!(abstractInterpret(c1, preContexts)) ||| !(abstractInterpret(c2, preContexts)))
                g
                
            (* compute the edgeTag but for the label and goto command. (The edgeTag holds the dfr, resetContext and modeContext)
               given a list of preContext a label and a computeMode function, compute for each preContext and the label param the postContext using
               the computeMode function.
             *)
            let computeEdgeMode label preContexts computeMode = 
                let computeModeEdge (ctx : ContextGraph.Context) = 
                    let mode = computeMode ctx.modeCtx label
                    let targetCtx = { ContextGraph.resetCtx = ctx.resetCtx; ContextGraph.modeCtx = mode; ContextGraph.constantCtx = ctx.constantCtx }
                    let edgeTag = setOfPairs.dfrI(!numVars, Pattern.Skip)
                    ContextGraph.E (ctx, targetCtx, ref edgeTag)

                ref (computeDoubleFlows (ContextGraph.newGraph <| List.map computeModeEdge preContexts))

            let doGoto label preContexts =
                let computeGotoMode premode postmode =
                    if premode = ContextGraph.Mode.Normal then postmode else premode

                computeEdgeMode label preContexts computeGotoMode

            let doLabel label preContexts = 
                let computeLabelMode premode postmode =
                    if premode = ContextGraph.Mode.Normal || premode = postmode then ContextGraph.Mode.Normal else premode

                computeEdgeMode label preContexts computeLabelMode

            (* the actual interpreter step - recursively interpret the command according to it's type and update it's attached graph with the result. *)
            let internalInterpret(CoreEx.AICmd(c, g, _) as c': CoreEx.Cmd, preContexts : ContextGraph.Context list) : ContextGraph.graph ref =
                let g = match c with
                        |  CoreEx.Seq(c1,c2)        -> doCompose(c1, c2, preContexts, g)
                        |  CoreEx.Choice(c1,c2)     -> doChoice(c1, c2, preContexts,g)
                        |  CoreEx.Skip              -> computeAssignmentGraph(c', 1, Core.Var 1, preContexts)
                        |  CoreEx.Goto(label)       -> doGoto (ContextGraph.Mode.Label(label)) preContexts
                        |  CoreEx.Label(label)      -> doLabel (ContextGraph.Mode.Label(label)) preContexts
                        |  CoreEx.Asgn(i, e)        -> computeAssignmentGraph(c', i, e, preContexts)
                        |  CoreEx.Loop(i, c)        -> doLoop(i, c, preContexts, g)
                (* send event that command graph was updated *)
                commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c', !g))
                g

            (* returns true if command c must be re-interpreted. This will be so if current pre-contexts are
               not a sub-set of the pre-contexts of the graph attached to command c *)
            let shouldUpdateCommandGraph(c,preContexts) =
                let g = CoreEx.graph(c)
                not (ContextGraph.preContextsIn(preContexts, !g))

            (* get reference to graph attached to command c *)
            let g = CoreEx.graph(c)
            let () = debugPrint("Started analysing command:\n")
            let () = debugPrint(CoreEx.prt(c))
            let () = if (shouldUpdateCommandGraph(c,preContexts)) then
                        g := !(internalInterpret(c, preContexts))

                     else () (* if graph doesn't need to be updated - do nothing *)
            let () = debugPrint("Finished analysing command:\n" + CoreEx.prt(c) + "result graph:\n")
            let () = debugPrintG(!g)
            let () = debugPrint("============================================\n")

            g

        (* initialize "global" identifier. *)
        let () = (numVars := Core.NumOfVars(c))
        (* Attach a context graph to each command, and convert each loop body c to "if { Skip} else { c }". *)
        let cExtended = CoreEx.extendedAbsIntAST(c)

        (* start running the abstract interpreter with a pre-contexts list containing only the empty context,
           since at first we assume no contexts. *)
        let emptyCtx = ContextGraph.makeEmptyContext(!numVars)
        let res = abstractInterpret(cExtended, [emptyCtx])
        !res

    member x.resultText(cmd, graph : ContextGraph.graph) =
        let numOfVars = Core.NumOfVars cmd
        let boundedLinear = ref [1..numOfVars]
        let boundedPolynomial = ref [1..numOfVars]
        let vt = Parser.parserLastVarToIndexMap()

        let printVar var = if vt.ContainsKey(var) then vt.[var] else "_"
        let rec printVars = function
            | [] -> ""
            | i::[] -> printVar i
            | i::rest -> printVar i + ", " + printVars rest

        for p in graph.Keys do
            for et in graph.[p].Values do
                match !et with
                    | (setOfPairs.Dfr(M,_)) ->
                            let (notboundedPolynomial', _) = sparseMatrix.classify(M, numOfVars, AbstractDomain.exponentialAtLeast)
                            let (notboundedLinear', _) = sparseMatrix.classify(M, numOfVars, AbstractDomain.linearPolynomial)
                            boundedPolynomial := !boundedPolynomial -- notboundedPolynomial'
                            boundedLinear := !boundedLinear -- notboundedLinear'

        boundedPolynomial := !boundedPolynomial -- !boundedLinear
        let nonbounded = List.filter (fun v -> not (!boundedPolynomial |> utils.contains v)) [1..numOfVars] -- !boundedLinear

        "\n\nVARS: " + numOfVars.ToString() + 
        (if (!boundedLinear).Length > 0 then "\nBounded Linearly: " + printVars !boundedLinear else "") +
        (if (!boundedPolynomial).Length > 0 then "\nBounded Polynomialy: " + printVars !boundedPolynomial else "") +
        (if nonbounded.Length > 0 then "\nExponential At Least: " + printVars nonbounded else "")

    (* set the debug output mode *)
    member x.setDebugMode(mode : bool) = Debug := mode

let absInt = AbstractInterpreter()